Adds 24 string rewrites addressing some of the low hanging rewrite proof
holes in SMT-LIB and our regressions.

It also applies a workaround for the Twine issue
[cvc5#1216](pypa/twine#1216).

It also uses Twine to check the generated wheels and the
`--skip-existing` option in Twine to continue uploading files if they
already exist.

Signed-off-by: Robert Bradshaw <robertwb@gmail.com>

These rewrites have not shown to be important in practice and moreover
are cumbersome to represent in proofs.

The behavior of the extended rewriter still is able to accomplish these
rewrites.

The extended rewriter is modified slightly in this PR to be more robust
in general with further changes.

These are 8 tests for the conjecture generator. I have removed any
irrelevant commands that I could identify, including assertions.

cvc5 takes <1 second to report 'unsat' for each test so long as the
unsat core tester is disabled. Based on my observations cvc5 cannot
solve them with induction switched on and conjecture generation switched
off, making conjecture generation essential to get a quick 'unsat'
response from the solver.

These tests will help ensure that I do not worsen the performance of the
conjecture generator as I clean it up. They might also help us identify
which changes to other components of cvc5 can impact the conjecture
generator.

Fixes cvc5#11520

This operation will be at the heart of ~5 forthcoming proof rules. 

This PR deletes the primative `Word::noOverlapWith` (which wasn't
directional and had a more complicated meaning) in favor of this new
utility.

A rewrite that relies on this utility is demoted to the extended
rewriter.

Unit tests are added for this utility.

This adds the default implementation of a proof logger (for cpc proofs).

It also adds some logic to ensure proof logging is used only in valid
configurations.

This adds the Eunoia definition of the evaluation methods for the
SMT-LIB standard operators `str.replace_re` and `str.replace_re_all`,
and the cvc5-specific extension `str.indexof_re`.

It also updates the strings rewrite to call the reference
implementations of these rules, which was missed in a previous PR.

Note these evaluators call `$str_eval_str_in_re` as a submethod, which
would benefit automatically from future optimizations to this method.

Towards filling remaining proof holes.

Furthermore adds this case to the Eunoia signature for `evaluate`.

Requires 4 new RARE rewrites for ITE lifting, and 4 for reasoning about
min/max terms.

A separate step is necessary to partition the expert RARE rewrites /
non-expert ones, after which I will ensure the includes are fully
disjoint.

…1543)

The `cong` rule of `Uf.eo` uses `$nary_reverse` in its conclusion.
Import `programs/Nary.eo` to resolve this issue.

In `Nary.eo`, the type `Int` from `theories/Arith.eo` is used in
`$nary_prefix` and `$nary_subsequence`.
Import `theories/Arith.eo` to resolve this issue.

Because `theories/Arith.eo` imports `theories/Builtin.eo`, which imports
`programs/Utils.eo`, the import of `programs/Utils.eo` in
`programs/Nary.eo` is no longer needed. Remove this include.

Signed-off-by: ciaran <ciaran.dunne@inria.fr>

This splits the definitions of arith/bv conversion functions to their
own theory file and adds the 2 existing theory rewrites for eliminating
these two operators via reductions to the CPC+Eunoia signature.

…5#11582)

I think the implementation of `ConjectureGenerator::check()` will read
better if it is split across a few helper functions.

Also makes minor modifications to the reduction utility to make it
consistent with the style of the other reductions.

…verlap reasoning (cvc5#11580)

This adds a four new ad-hoc theory rewrites for strings, including their
internal and Eunoia definitions.

3 of these rules are exercized extensively in SMT-LIB, and all 4 will be
covered in regressions once they are enabled.

They are each based around the notion of computing "overlaps". 

This will be used to elaborate proofs for 4 macro theory rewrites, to be
added in followup PRs.

Note: in their current form, these rules *cannot* be applied to
sequences, as it is non-trivial in general to *prove* the distinctness
of sequence characters.

Furthermore note that the existing definition of
`ProofRule::CONCAT_CPROP` will be later simplified to use the
`$str_has_overlap` utility (it currently computes the *size* of a
maximal overlap using `$str_overlap`, which can be simplified by an
internal elaboration step). The signature definition of this rule at the
moment is theoretically unsound for sequences, since we do not prove the
distinctness of sequence characters (although cvc5 internally will do
so).

CI currently builds cvc5 on Ubuntu 20.04 to ensure compatibility with
this older OS version for dynamically linked binaries. However, the
Ubuntu 20.04 Actions runner image will begin deprecation on 2025-02-01
and will be fully unsupported by 2025-04-01 (see
[notice](actions/runner-images#11101) here).
Therefore, this PR updates the runners to Ubuntu 22.04.

Additionally, this PR removes a workaround previously required for old
versions of ccache.

This change has a similar motivation to
cvc5#11501.

In particular, it is unintuitive to store an internal kind as an
argument to a proof rule which is exported. Instead, we store the
conclusion of the rule, analogous to ARITH_POLY_NORM. The Eunoia
definition can be made more elegant.

This adds proof elaboration for the recently itnroduced rule
`MACRO_ARRAYS_NORMALIZE_OP` in terms of small step rewrites that RARE
can handle.

Notice that `MACRO_ARRAYS_NORMALIZE_OP` is now attempted *prior* to
RARE, meaning this rule now is used to preprocess >99% of array rewrites
into single steps for RARE.

…vc5#11590)

This is work towards simplifying CPC and its formalism in Eunoia for the
sake of further verification efforts.

Makes the following changes:
- `produceUnsatCores`, `checkUnsatCores` are promoted to "common" as
they are part of our core infrastructure.
- `fullSaturateQuant`/`enumInst` (which are an alias of one another) are
promoted to "common". The justification is that this option is
recommended to be used in addition to any other combination of options
for quantifiers for those that prefer more effort + timeouts to
unknowns.
- Similarly, `decisionMode` is promoted to "common", as it is intended
to be used in combination with all other options, e.g. in portfolios.
- `unconstrainedSimp` and `sortInference` are demoted to "expert" since
they do not meet the requirements of producing *models* (as well as
proofs).
- A new expert option `varEntEqElimQuant` now guards a (seldom used)
rewrite for quantifiers+strings that is hard to justify.

The fix involves the use of unused variables to ensure we can miniscope
OR when reversing elaboration of prenex. Both were leading to proof
holes which this PR fixes.

The second ensures we add unique variables for shared subformulas. For
example:
forall x. (forall y. P(y) or forall y. P(y))
we previously would prenex to:
forall x z z. (P(z) or P(z))
now we prenex to
forall x z w. (P(z) or P(w))
While it is technically legal to prenex to the same variable when their
polarity is the same, it is harder to justify and leads to unexpected
shadowing.

---------

Co-authored-by: Abdalrhman Mohamed <abdoo8080@outlook.com>

…ION (cvc5#11497)

Review cvc5#11476 first.

This fixes a bug in how RARE proof reconstruction works for macro
elaboration.

In particular, our subgoal tracking was incorrect if a macro was
elaboarted to a single TRUST step as a subgoal, since the updater
updates the current proof node in-place. The PR
cvc5#11441 introduces a case in our
regressions for this.

To fix this, I've refactored the post-processor to a more elegant
version which runs the proof node updater recursively. It tracks the
depth of how many trust steps we've expanded in the current context
using a `d_traversing` vector.

This makes explicit tracking of subgoals unecessary, the RARE proof
reconstruction method is cleaned up as a result.

This is necessary to build against libc++ in newer LLVM versions.

Includes one regression where cvc5 fails to generate a proof, due to
non-determinism in the rewriter. I've opened
cvc5/cvc5-projects#760 to track this.

…vc5#11441)

Adds 2 new RARE rules that suffice to prove these rules. FYI @Lachnitt 

This fills all the remaining known holes for (linear) arithmetic
rewriting.

- Add .toml files for the existing kinds
- Add python script to generate type_checker.cpp

---------

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>

This fixes issues in C++ `deadPool` test and resolves nightly memory
leak failure.

This adds a simple utilty for attempting to reconstruction proofs for
unhandled arithmetic theory lemmas.

In particular, lemmas marked `ARITH_DIO_LEMMA` typically can be
reconstructed using substitution+rewriting, leveraging the rewrite rules
from cvc5#11441.

This fills in the last remaining holes for arithmetic theory lemmas in
the regressions and SMT-LIB.

---------

Co-authored-by: Abdalrhman Mohamed <abdoo8080@outlook.com>

…vc5#11808)

This makes the essential changes to support the new defaults of
declare-parameterized-const.

It also fixes some misplaced attributes which will be caught by ethos
when it is updated.

It is redundant to apply `$singleton_elim` to heads of RARE rules, as we
know heads are always matched syntactically.

This makes the Eunoia definitions clearer and should help performance
slightly.

The evaluator is primarily used for sygus symmetry breaking and for RARE
proof reconstruction. Moreover repeat is eliminated during rewriting, so
this bug had a very minimal impact. I discovered it due to a proof hole
that appeared in my dev branch related to RARE reconstruction.